Inference at * 2 1 1 1 1 1 1 1 
Iof proof for Lemma less-fast-fib:

.....antecedent..... NILNIL

1. f : 
1. n, a, b:.
1. {m:| 
1. {k:. (a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
2. n : 
3. v : 
4. k:. (1 = fib(k))  ((k  0)  (0 = 0))  ((0 < k)  (0 = fib(k - 1)))  (v = fib(n+k))
5. f(n,1,0) = v
  1 = fib(0) 

latex

 by (RecUnfold `fib` 0) 
CollapseTHEN ((Reduce 0) 
THEN (Auto)) 

latex

T.

Definitions

(i = j), x:A. B(x), #$n